Galois connections are a foundational tool for structuring abstraction insemantics and their use lies at the heart of the theory of abstractinterpretation. Yet, mechanization of Galois connections remains limited torestricted modes of use, preventing their general application in mechanizedmetatheory and certified programming. This paper presents constructive Galois connections, a variant of Galoisconnections that is effective both on paper and in proof assistants; iscomplete with respect to a large subset of classical Galois connections; andenables more general reasoning principles, including the "calculational" styleadvocated by Cousot. To design constructive Galois connection we identify a restricted mode of useof classical ones which is both general and amenable to mechanization independently-typed functional programming languages. Crucial to our metatheoryis the addition of monadic structure to Galois connections to control a"specification effect". Effectful calculations may reason classically, whilepure calculations have extractable computational content. Explicitly movingbetween the worlds of specification and implementation is enabled by ourmetatheory. To validate our approach, we provide two case studies in mechanizing existingproofs from the literature: one uses calculational abstract interpretation todesign a static analyzer, the other forms a semantic basis for gradual typing.Both mechanized proofs closely follow their original paper-and-pencilcounterparts, employ reasoning principles not captured by previousmechanization approaches, support the extraction of verified algorithms, andare novel.
展开▼
